package no.uio.ifi.cop.prover;

import java.util.LinkedList;

import no.uio.ifi.cop.common.Log;
import no.uio.ifi.cop.cl.Term;
import no.uio.ifi.cop.cl.Axiom;
import no.uio.ifi.cop.cl.Conjunction;
import no.uio.ifi.cop.cl.Substitution;
import no.uio.ifi.cop.cl.RHS;

/**
 * This class is used to store proof trees which
 * then can be formatted/printed.
 *
 * @version 1.0
 * @author  bjarneh@ifi.uio.no
 */

public class Node{

    private static int counter = 1;
    private static int max     = Integer.MAX_VALUE;

    private int id; 
    private Conjunction facts;
    private Axiom axiom;
    private Substitution substitution;
    private LinkedList<Node> children;

    public Node(){
        id = counter++;
        children = new LinkedList<Node>();
    }

    public Node(Conjunction conjunction){
        this();
        addResult( conjunction );
    }

    public static void resetCounter(){
        counter = 1;
    }

    public Conjunction getFacts(){
        return facts;
    }

    public int getId(){
        return id;
    }

    public void addResult(Conjunction conjunction){
        facts = conjunction;
    }

    public void addAxiom(Axiom ax){
        axiom = ax;
    }

    public void addSubstitution(Substitution subst){
        substitution = subst;
    }

    public void extend( Node result ){
        children.add( result );
    }

    public String toString(){
        return "@Node (use dotGraph() to see me)";
    }

    protected void setMax(int max){
        this.max = max;
    }

    protected void dotGraph(StringBuilder sb){

        if( id >= max ){ return; }

        boolean labelDrawn = false;

        String      tmpStr;

        for( Node n : children ){
            if( ! labelDrawn ){
                tmpStr  = "  \"%d: %s\" -> \"%d: %s\" ";
                tmpStr += " [ label = \" %s => %s | %s \", fontsize = 7 ];\n";
                sb.append(String.format(tmpStr, id,getFacts(), 
                          n.getId(), n.getFacts(), 
                          axiom.getLHS(), axiom.getRHS(), substitution));
                labelDrawn = true;
            }else{
                tmpStr = "  \"%d: %s\" -> \"%d: %s\";\n";
                sb.append(String.format(tmpStr, id,getFacts(), n.getId(), n.getFacts()));
            }
            n.dotGraph(sb);
        }
    }
}
